L:MsgA List. ma-is-empty((L))  reduce(M,x. ma-is-empty(M) & x;True;L) 

latex

Definitions	p  q, , true, ma-is-empty(M), reduce(f;k;as), Prop, P  Q, P & Q, P  Q, P  Q, True, x:A. B(x), t  T, MsgA, b
Lemmas	msga wf, ma-join-list-is-empty, true wf, ma-is-empty wf, assert wf, reduce wf, btrue wf, bool wf, band wf, assert of band, iff functionality wrt iff